WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) foldr#3(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> Cons(Pair(x40,x56),foldr#3(product_ms_ns_2(x40),x14,x6)) main(x2,x1) -> foldr#3(product_ms_ns(x1),Nil(),x2) - Signature: {foldr#3/3,main/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3,main} and constructors {Cons,Nil,Pair ,product_ms_ns,product_ms_ns_2} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs foldr#3#(x8,x12,Nil()) -> c_1() foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) main#(x2,x1) -> c_4(foldr#3#(product_ms_ns(x1),Nil(),x2)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: foldr#3#(x8,x12,Nil()) -> c_1() foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) main#(x2,x1) -> c_4(foldr#3#(product_ms_ns(x1),Nil(),x2)) - Weak TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) foldr#3(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> Cons(Pair(x40,x56),foldr#3(product_ms_ns_2(x40),x14,x6)) main(x2,x1) -> foldr#3(product_ms_ns(x1),Nil(),x2) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1,c_1/0,c_2/2 ,c_3/1,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair ,product_ms_ns,product_ms_ns_2} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {2,3,4}. Here rules are labelled as follows: 1: foldr#3#(x8,x12,Nil()) -> c_1() 2: foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) 3: foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) 4: main#(x2,x1) -> c_4(foldr#3#(product_ms_ns(x1),Nil(),x2)) * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) main#(x2,x1) -> c_4(foldr#3#(product_ms_ns(x1),Nil(),x2)) - Weak DPs: foldr#3#(x8,x12,Nil()) -> c_1() - Weak TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) foldr#3(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> Cons(Pair(x40,x56),foldr#3(product_ms_ns_2(x40),x14,x6)) main(x2,x1) -> foldr#3(product_ms_ns(x1),Nil(),x2) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1,c_1/0,c_2/2 ,c_3/1,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair ,product_ms_ns,product_ms_ns_2} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) -->_1 foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)):2 -->_2 foldr#3#(x8,x12,Nil()) -> c_1():4 -->_1 foldr#3#(x8,x12,Nil()) -> c_1():4 -->_2 foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)):1 2:S:foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) -->_1 foldr#3#(x8,x12,Nil()) -> c_1():4 -->_1 foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)):2 3:S:main#(x2,x1) -> c_4(foldr#3#(product_ms_ns(x1),Nil(),x2)) -->_1 foldr#3#(x8,x12,Nil()) -> c_1():4 -->_1 foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)):1 4:W:foldr#3#(x8,x12,Nil()) -> c_1() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: foldr#3#(x8,x12,Nil()) -> c_1() * Step 4: RemoveHeads WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) main#(x2,x1) -> c_4(foldr#3#(product_ms_ns(x1),Nil(),x2)) - Weak TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) foldr#3(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> Cons(Pair(x40,x56),foldr#3(product_ms_ns_2(x40),x14,x6)) main(x2,x1) -> foldr#3(product_ms_ns(x1),Nil(),x2) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1,c_1/0,c_2/2 ,c_3/1,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair ,product_ms_ns,product_ms_ns_2} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) -->_1 foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)):2 -->_2 foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)):1 2:S:foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) -->_1 foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)):2 3:S:main#(x2,x1) -> c_4(foldr#3#(product_ms_ns(x1),Nil(),x2)) -->_1 foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)):1 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(3,main#(x2,x1) -> c_4(foldr#3#(product_ms_ns(x1),Nil(),x2)))] * Step 5: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) - Weak TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) foldr#3(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> Cons(Pair(x40,x56),foldr#3(product_ms_ns_2(x40),x14,x6)) main(x2,x1) -> foldr#3(product_ms_ns(x1),Nil(),x2) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1,c_1/0,c_2/2 ,c_3/1,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair ,product_ms_ns,product_ms_ns_2} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) foldr#3(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> Cons(Pair(x40,x56),foldr#3(product_ms_ns_2(x40),x14,x6)) foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) * Step 6: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) - Weak TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) foldr#3(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> Cons(Pair(x40,x56),foldr#3(product_ms_ns_2(x40),x14,x6)) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1,c_1/0,c_2/2 ,c_3/1,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair ,product_ms_ns,product_ms_ns_2} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) and a lower component foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) Further, following extension rules are added to the lower component. foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3#(product_ms_ns(x3),Nil(),x1) foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) - Weak TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) foldr#3(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> Cons(Pair(x40,x56),foldr#3(product_ms_ns_2(x40),x14,x6)) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1,c_1/0,c_2/2 ,c_3/1,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair ,product_ms_ns,product_ms_ns_2} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)) -->_2 foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) ,foldr#3#(product_ms_ns(x3),Nil(),x1)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns(x3),Nil(),x1)) ** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns(x3),Nil(),x1)) - Weak TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) foldr#3(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> Cons(Pair(x40,x56),foldr#3(product_ms_ns_2(x40),x14,x6)) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1,c_1/0,c_2/1 ,c_3/1,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair ,product_ms_ns,product_ms_ns_2} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns(x3),Nil(),x1)) ** Step 6.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns(x3),Nil(),x1)) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1,c_1/0,c_2/1 ,c_3/1,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair ,product_ms_ns,product_ms_ns_2} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- Cons :: ["A"(14) x "A"(14)] -(14)-> "A"(14) Nil :: [] -(0)-> "A"(0) Nil :: [] -(0)-> "A"(12) product_ms_ns :: ["A"(0)] -(3)-> "A"(3) product_ms_ns :: ["A"(0)] -(7)-> "A"(7) foldr#3# :: ["A"(3) x "A"(0) x "A"(14)] -(7)-> "A"(0) c_2 :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "Cons_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "Nil_A" :: [] -(0)-> "A"(1) "c_2_A" :: ["A"(0)] -(0)-> "A"(1) "product_ms_ns_A" :: ["A"(0)] -(1)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> c_2(foldr#3#(product_ms_ns(x3),Nil(),x1)) 2. Weak: ** Step 6.b:1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) - Weak DPs: foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3#(product_ms_ns(x3),Nil(),x1) foldr#3#(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3#(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) - Weak TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x3),Nil(),Cons(x2,x1)) -> foldr#3(product_ms_ns_2(x2) ,foldr#3(product_ms_ns(x3),Nil(),x1) ,x3) foldr#3(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> Cons(Pair(x40,x56),foldr#3(product_ms_ns_2(x40),x14,x6)) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1,c_1/0,c_2/2 ,c_3/1,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair ,product_ms_ns,product_ms_ns_2} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- Cons :: ["A"(13) x "A"(13)] -(13)-> "A"(13) Cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) Nil :: [] -(0)-> "A"(0) Nil :: [] -(0)-> "A"(7) Pair :: ["A"(0) x "A"(0)] -(0)-> "A"(15) foldr#3 :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) product_ms_ns :: ["A"(0)] -(0)-> "A"(0) product_ms_ns :: ["A"(15)] -(0)-> "A"(15) product_ms_ns :: ["A"(1)] -(0)-> "A"(1) product_ms_ns_2 :: ["A"(0)] -(0)-> "A"(15) product_ms_ns_2 :: ["A"(0)] -(0)-> "A"(0) product_ms_ns_2 :: ["A"(0)] -(0)-> "A"(11) foldr#3# :: ["A"(15) x "A"(0) x "A"(13)] -(5)-> "A"(3) c_3 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "Cons_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "Nil_A" :: [] -(0)-> "A"(1) "Pair_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "c_3_A" :: ["A"(0)] -(0)-> "A"(1) "product_ms_ns_2_A" :: ["A"(0)] -(0)-> "A"(1) "product_ms_ns_A" :: ["A"(0)] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: foldr#3#(product_ms_ns_2(x40),x14,Cons(x56,x6)) -> c_3(foldr#3#(product_ms_ns_2(x40),x14,x6)) 2. Weak: WORST_CASE(?,O(n^2))